The safety of mobile robots in dynamic environments is predicated on makingsure that they do not collide with obstacles. In support of such safetyarguments, we analyze and formally verify a series of increasingly powerfulsafety properties of controllers for avoiding both stationary and movingobstacles: (i) static safety, which ensures that no collisions can happen withstationary obstacles, (ii) passive safety, which ensures that no collisions canhappen with stationary or moving obstacles while the robot moves, (iii) thestronger passive friendly safety in which the robot further maintainssufficient maneuvering distance for obstacles to avoid collision as well, and(iv) passive orientation safety, which allows for imperfect sensor coverage ofthe robot, i. e., the robot is aware that not everything in its environmentwill be visible. We complement these provably correct safety properties withliveness properties: we prove that provably safe motion is flexible enough tolet the robot still navigate waypoints and pass intersections. We use hybridsystem models and theorem proving techniques that describe and formally verifythe robot's discrete control decisions along with its continuous, physicalmotion. Moreover, we formally prove that safety can still be guaranteed despitesensor uncertainty and actuator perturbation, and when control choices for moreaggressive maneuvers are introduced. Our verification results are generic inthe sense that they are not limited to the particular choices of one specificcontrol algorithm but identify conditions that make them simultaneously applyto a broad class of control algorithms.
展开▼
